﻿module ForwardInferenceRules

open Types
open TruthFunctions
open Utilities
open Reduce

//
// Predicates for NAL
//
let measureTime(s, p) = false            // *** TODO complete this func
let concurrent(s, p) = false            // *** TODO complete this func
let notImplication =  function | Imp(_) -> false | _ -> true
let notSet = function | IntSet _ | ExtSet _ -> false | _ -> true

let forwardRules = 
    [|
    (fun (tv1, tv2 : Truth) -> function Inh(s1, p1), Sim(s2, p2) when s1 = s2 && p1 = p2 && s1 <> p1 -> [(Inh(s1, p1), int((1.0f, 1.0f), tv1))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(s1, p), Inh(s2, _) when s1 <> p && s1 = s2 -> [(Inh(p, s1), cnv(tv1))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(s, p1), Inh(_, p2) when s <> p1 && p1 = p2 -> [(Inh(p1, s), cnv(tv1))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(s1, p), Imp(s2, _) when s1 <> p && s1 = s2 -> [(Imp(p, s1), cnv(tv1))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(s, p1), Imp(_, p2) when s <> p1 && p1 = p2 -> [(Imp(p1, s), cnv(tv1))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function ConImp(s1, p), ConImp(s2, _) when s1 <> p && s1 = s2 -> [(ConImp(p, s1), cnv(tv1))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function ConImp(s, p1), ConImp(_, p2) when s <> p1 && p1 = p2 -> [(ConImp(p1, s), cnv(tv1))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function PreImp(s1, p), PreImp(s2, _) when s1 <> p && s1 = s2 -> [(PreImp(p, s1), cnv(tv1))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function PreImp(s, p1), PreImp(_, p2) when s <> p1 && p1 = p2 -> [(PreImp(p1, s), cnv(tv1))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function RetImp(s1, p), RetImp(s2, _) when s1 <> p && s1 = s2 -> [(RetImp(p, s1), cnv(tv1))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function RetImp(s, p1), RetImp(_, p2) when s <> p1 && p1 = p2 -> [(RetImp(p1, s), cnv(tv1))] | _ -> [])


    (fun (tv1, tv2 : Truth) -> function Sim(ExtSet(s), ExtSet(p)), _ when s <> p -> [(Inh(ExtSet(s), ExtSet(p)), tv1)
                                                                                     (Inh(ExtSet(p), ExtSet(s)), tv1)] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Sim(IntSet(s), IntSet(p)), _ when s <> p -> [(Inh(IntSet(s), IntSet(p)), tv1)
                                                                                     (Inh(IntSet(p), IntSet(s)), tv1)] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(Not(s), p1), Imp(_, p2) when s <> p1 && p1 = p2 -> [(Imp(Not(p1), s), cnt(tv1))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(Not(s1), p), Imp(s2, _) when s1 <> p && s1 = s2 -> [(Imp(Not(p), s1), cnt(tv1))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function ConImp(Not(s), p1), Imp(_, p2) when s <> p1 && p1 = p2 -> [(ConImp(Not(p1), s), cnt(tv1))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function ConImp(Not(s1), p), Imp(s2, _) when s1 <> p && s1 = s2 -> [(ConImp(Not(p), s1), cnt(tv1))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function PreImp(Not(s), p1), Imp(_, p2) when s <> p1 && p1 = p2 -> [(PreImp(Not(p1), s), cnt(tv1))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function PreImp(Not(s1), p), Imp(s2, _) when s1 <> p && s1 = s2 -> [(PreImp(Not(p), s1), cnt(tv1))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function RetImp(Not(s), p1), Imp(_, p2) when s <> p1 && p1 = p2 -> [(RetImp(Not(p1), s), cnt(tv1))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function RetImp(Not(s1), p), Imp(s2, _) when s1 <> p && s1 = s2 -> [(RetImp(Not(p), s1), cnt(tv1))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Not(s), x when fst(tv1) < 0.5f -> [(s, neg(tv1))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function s, x when fst(tv1) < 0.5f -> [(Not(s), neg(tv1))] | _ -> [])
    
    (fun (tv1, tv2 : Truth) -> function Inh(a, b1), Inh(b2, c) when a <> c && b1 = b2 -> [(Inh(a, c), ded(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(a1, b), Inh(a2, c) when b <> c && a1 = a2 -> [(Inh(b, c), ind(tv1, tv2))
                                                                                          (Inh(c, b), ind(tv2, tv1))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(a, c1), Inh(b, c2) when a <> b && c1 = c2 -> [(Inh(a, b), abd(tv1, tv2)) 
                                                                                          (Inh(b, a), abd(tv2, tv1))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(a, b1), Inh(b2, c) when a <> c && b1 = b2 -> [(Inh(c, a), exe(tv1, tv2))] | _ -> [])

    (fun (tv1, tv2 : Truth) -> function Inh(s1, p1), Inh(p2, s2) when s1 = s2 && p1 = p2 -> [(Sim(s1, p1), int(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Sim(s1, p1) , Inh(s2, p2) when s1 = s2 && p1 = p2 -> [(Inh(s1, p2), uni(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(p, m1), Inh(s, m2) when s <> p && m1 = m2 -> [(Sim(s, p), com(tv2, tv1))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(m1, p), Inh(m2, s) when s <> p && m1 = m2 -> [(Sim(s, p), com(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(m1, p), Sim(s, m2) when s <> p && m1 = m2 -> [(Inh(s, p), ana(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(p, m1), Sim(s, m2) when s <> p && m1 = m2 -> [(Inh(p, s), ana(tv2, tv1))] | _ -> []) 
    (fun (tv1, tv2 : Truth) -> function Sim(m1, p), Sim(s, m2) when s <> p && m1 = m2 -> [(Sim(s, p), res(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(p, m1), Inh(s, m2) when s <> p && m1 = m2 && notSet(s) && notSet(p) && noCommonTerm(s, p) 
                                        -> [(Inh(IntInt(set [s; p]), m1), int(tv1, tv2))
                                            (Inh(ExtInt(set [s; p]), m1), uni(tv1, tv2))
                                            (Inh(IntDif(s, p), m1), dif(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(m1, p), Inh(m2, s) when s <> p && m1 = m2 && notSet(s) && notSet(p) && noCommonTerm(s, p) 
                                        -> [(Inh(ExtInt(set [s; p]), m1), int(tv1, tv2))
                                            (Inh(IntInt(set [s; p]), m1), uni(tv1, tv2))
                                            (Inh(ExtDif(s, p), m1), dif(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(s, m1), Inh(IntInt(p), m2) when m1 = m2 && p |> Set.contains s -> [(Inh(IntInt(p |> Set.remove s), m1), pnn(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(s, m1), Inh(ExtInt(p), m2) when m1 = m2 && p |> Set.contains s -> [(Inh(ExtInt(p |> Set.remove s), m1), npp(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(s1, m1), Inh(IntDif(s2, p), m2) when s2 <> p && m1 = m2 && s1 = s2 -> [(Inh(p, m1), pnp(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(s1, m1), Inh(IntDif(p, s2), m2) when s2 <> p && m1 = m2 && s1 = s2 -> [(Inh(p, m1), nnn(tv1, tv2))] | _ -> [])  
    (fun (tv1, tv2 : Truth) -> function Inh(m1, s), Inh(m2, ExtInt(p)) when m1 = m2 && p |> Set.contains s -> [(Inh(m1, ExtInt(p |> Set.remove s)), pnn(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(m1, s), Inh(m2, IntInt(p)) when m1 = m2 && p |> Set.contains s -> [(Inh(m1, IntInt(p |> Set.remove s)), npp(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(m1, s1), Inh(m2, ExtDif(s2, p)) when m1 = m2 && s1 = s2 && s1 <> p -> [(Inh(m1, p), pnp(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(m1, s1), Inh(m2, ExtDif(p, s2)) when m1 = m2 && s1 = s2 && s1 <> p -> [(Inh(m1, p), nnn(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(m1, p), Imp(s, m2) when s <> p && m1 = m2 -> [(Imp(s, p), ded(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(p, m1), Imp(s, m2) when s <> p && m1 = m2 -> [(Imp(s, p), abd(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function ConImp(p, m1), ConImp(s, m2) when s <> p && m1 = m2 -> [(ConImp(s, p), abd(tv1, tv2))
                                                                                                (PreImp(s, p), abd(tv1, tv2))
                                                                                                (RetImp(s, p), abd(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function PreImp(p, m1), PreImp(s, m2) when s <> p && m1 = m2 -> [(ConImp(s, p), abd(tv1, tv2))
                                                                                                (PreImp(s, p), abd(tv1, tv2))
                                                                                                (RetImp(s, p), abd(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function RetImp(p, m1), RetImp(s, m2) when s <> p && m1 = m2 -> [(ConImp(s, p), abd(tv1, tv2))
                                                                                                (PreImp(s, p), abd(tv1, tv2))
                                                                                                (RetImp(s, p), abd(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(m1, p), Imp(m2, s) when s <> p && m1 = m2 -> [(Imp(s, p), ind(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function PreImp(m1, p), PreImp(m2, s) when s <> p && m1 = m2 -> [(ConImp(s, p), ind(tv1, tv2))
                                                                                                (PreImp(s, p), ind(tv1, tv2))
                                                                                                (RetImp(s, p), ind(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function ConImp(m1, p), ConImp(m2, s) when s <> p && m1 = m2 -> [(ConImp(s, p), ind(tv1, tv2))
                                                                                                (PreImp(s, p), ind(tv1, tv2))
                                                                                                (RetImp(s, p), ind(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function RetImp(m1, p), RetImp(m2, s) when s <> p && m1 = m2 -> [(ConImp(s, p), ind(tv1, tv2))
                                                                                                (PreImp(s, p), ind(tv1, tv2))
                                                                                                (RetImp(s, p), ind(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(p, m1), Imp(m2, s) when s <> p && m1 = m2 -> [(Imp(s, p), exe(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function PreImp(p, m1), PreImp(m2, s) when s <> p && m1 = m2 -> [(RetImp(s, p), exe(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function ConImp(p, m1), ConImp(m2, s) when s <> p && m1 = m2 -> [(ConImp(s, p), exe(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(s1, p1), Imp(p2, s2) when s1 <> p1 && s1 = s2 && p1 = p2 -> [(Equ(s1, p1), int(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function ConImp(s1, p1), ConImp(p2, s2) when s1 <> p1 && s1 = s2 && p1 = p2 -> [(ConEqu(s1, p1), int(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function PreImp(s1, p1), RetImp(p2, s2) when s1 <> p1 && s1 = s2 && p1 = p2 -> [(PreEqu(s1, p1), int(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function RetImp(s1, p1), PreImp(p2, s2) when s1 <> p1 && s1 = s2 && p1 = p2 -> [(PreEqu(s1, p1), int(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(p, m1), Imp(s, m2) when s <> p && m1 = m2 -> [(Equ(s, p), com(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function PreImp(p, m1), PreImp(s, m2) when s <> p && m1 = m2 
                                        -> [(ConEqu(s, p), com(tv1, tv2))
                                            (PreEqu(s, p), com(tv1, tv2))
                                            (PreEqu(p, s), com(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function ConImp(p, m1), ConImp(s, m2) when s <> p && m1 = m2 -> [(ConEqu(s, p), com(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function RetImp(p, m1), RetImp(s, m2) when s <> p && m1 = m2 
                                        -> [(ConEqu(s, p), com(tv1, tv2))
                                            (PreEqu(s, p), com(tv1, tv2))
                                            (PreEqu(p, s), com(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(m1, p), Imp(m2, s) when s <> p && m1 = m2 -> [(Equ(s, p), com(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function PreImp(m1, p), PreImp(m2, s) when s <> p && m1 = m2 
                                        -> [(ConEqu(s, p), com(tv1, tv2))
                                            (PreEqu(s, p), com(tv1, tv2))
                                            (PreEqu(p, s), com(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function ConImp(m1, p), ConImp(m2, s) when s <> p && m1 = m2 -> [(ConEqu(s, p), com(tv1, tv2))] | _ -> [])

    (fun (tv1, tv2 : Truth) -> function Imp(m1, p), Equ(s, m2) when s <> p && m1 = m2 -> [(Imp(s, p), ana(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function PreImp(m1, p), PreEqu(s, m2) when s <> p && m1 = m2 -> [(PreImp(s, p), ana(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function PreImp(m1, p), ConEqu(s, m2) when s <> p && m1 = m2 -> [(PreImp(s, p), ana(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function ConImp(m1, p), ConEqu(s, m2) when s <> p && m1 = m2 -> [(ConImp(s, p), ana(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function RetImp(m1, p), PreEqu(s, m2) when s <> p && m1 = m2 -> [(RetImp(s, p), ana(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function RetImp(m1, p), ConEqu(s, m2) when s <> p && m1 = m2 -> [(RetImp(s, p), ana(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(p, m1), Equ(s, m2) when s <> p && m1 = m2 -> [(Imp(p, s), ana(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function PreImp(p, m1), ConEqu(s, m2) when s <> p && m1 = m2 -> [(PreImp(p, s), ana(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function ConImp(p, m1), ConEqu(s, m2) when s <> p && m1 = m2 -> [(ConImp(p, s), ana(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function RetImp(p, m1), PreEqu(s, m2) when s <> p && m1 = m2 -> [(RetImp(p, s), ana(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function RetImp(p, m1), ConEqu(s, m2) when s <> p && m1 = m2 -> [(RetImp(p, s), ana(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Equ(m1, p), Equ(s, m2) when s <> p && m1 = m2 -> [(Equ(s, p), res(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function PreEqu(m1, p), ConEqu(s, m2) when s <> p && m1 = m2 -> [(PreEqu(s, p), res(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function ConEqu(m1, p), PreEqu(s, m2) when s <> p && m1 = m2 -> [(PreEqu(s, p), res(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(p, m1), Imp(s, m2) when s <> p && m1 = m2 && noCommonTerm(s, p) 
                                        -> [(Imp(Or(set [p; s]),m1), int(tv1, tv2))
                                            (Imp(And(set [p; s]),m1), uni(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function ConImp(p, m1), ConImp(s, m2) when s <> p && m1 = m2 && noCommonTerm(s, p) 
                                        -> [(ConImp(Or(set [p; s]),m1), int(tv1, tv2))
                                            (ConImp(Par(set [p; s]),m1), uni(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function PreImp(p, m1), PreImp(s, m2) when s <> p && m1 = m2 && noCommonTerm(s, p) 
                                        -> [(PreImp(Or(set [p; s]),m1), int(tv1, tv2))
                                            (PreImp(Par(set [p; s]),m1), uni(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function RetImp(p, m1), RetImp(s, m2) when s <> p && m1 = m2 && noCommonTerm(s, p) 
                                        -> [(RetImp(Or(set [p; s]),m1), int(tv1, tv2))
                                            (RetImp(Par(set [p; s]),m1), uni(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(m1, p), Imp(m2, s) when s <> p && m1 = m2 && noCommonTerm(s, p) 
                                        -> [(Imp(m1, And(set [p; s])), int(tv1, tv2))
                                            (Imp(m1, Or(set [p; s])), uni(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function PreImp(m1, p), PreImp(m2, s) when s <> p && m1 = m2 && noCommonTerm(s, p) 
                                        -> [(PreImp(m1, Par(set [p; s])), int(tv1, tv2))
                                            (PreImp(m1, Or(set [p; s])), uni(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function ConImp(m1, p), ConImp(m2, s) when s <> p && m1 = m2 && noCommonTerm(s, p) 
                                        -> [(ConImp(m1, Par(set [p; s])), int(tv1, tv2))
                                            (ConImp(m1, Or(set [p; s])), uni(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function RetImp(m1, p), RetImp(m2, s) when s <> p && m1 = m2 && noCommonTerm(s, p) 
                                        -> [(RetImp(m1, Par(set [p; s])), int(tv1, tv2))
                                            (RetImp(m1, Or(set [p; s])), uni(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(s, m1), Imp(Or(p), m2) when m1 = m2 && p |> Set.contains s -> [(Imp(Or(p |> Set.remove s), m1), pnn(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(s, m1), Imp(And(p), m2) when m1 = m2 && p |> Set.contains s -> [(Imp(And(p |> Set.remove s), m1), npp(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(m1, s), Imp(m2, And(p)) when m1 = m2 && p |> Set.contains s -> [(Imp(m1, And(p |> Set.remove s)), pnn(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(m1, s), Imp(m2, Or(p)) when m1 = m2 && p |> Set.contains s -> [(Imp(m1, Or(p |> Set.remove s)), npp(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function m1, Imp(m2, p) when m1 = m2 && m1 <> p -> [(p, ded(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function m1, Imp(p, m2) when m1 = m2 && m1 <> p -> [(p, abd(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function m1, Equ(s, m2) when m1 = m2 && m1 <> s -> [(s, ana(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function m1, Equ(m2, s) when m1 = m2 && m1 <> s -> [(s, ana(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function s, And(p) when p |> Set.contains s -> [(And(p |> Set.remove s), pnn(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function s, Or(p) when p |> Set.contains s -> [(Or(p |> Set.remove s), npp(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(And(s), c), m when s |> Set.contains m && c <> m && notImpOrEqu(m) -> [(And(s |> Set.remove m), ded(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(And(s), c1), Imp(And(p), c2) when c1 = c2 && (s - p) |> Set.count = 1 -> [(s - p |> Set.minElement, abd(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(And(s), c), Imp(a, m) when a <> c && c <> m && s |> Set.contains m -> [(Imp(And(s |> Set.remove m), c), ded(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(And(s), c1), Imp(And(p), c2) when c1 = c2 && s - p |> Set.count = 1 && p - s |> Set.count = 1 -> [(Imp(s - p |> Set.maxElement, p - s |> Set.maxElement), abd(tv1, tv1))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(And(s), c), Imp(a, m) when a <> m && c <> a && s |> Set.contains a -> [(Imp(And(s |> Set.remove a |> Set.add m), c), ind(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(p, m1), Inh(s, m2) when s <> p && m1 = m2 
                                        -> [(Imp(Inh(p, IVar("X")), Inh(s, IVar("X"))), abd(tv1, tv2))
                                            (Equ(Inh(p, IVar("X")), Inh(s, IVar("X"))), com(tv1, tv2))
                                            (And(set [Inh(s, DVar("X")); Inh(p, DVar("X"))]), int(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(p, m1), Inh(s, m2) when s <> p && m1 = m2 
                                        -> [(PreImp(Inh(p, IVar("X")), Inh(s, IVar("X"))), abd(tv1, tv2))
                                            (PreEqu(Inh(p, IVar("X")), Inh(s, IVar("X"))), com(tv1, tv2))
                                            (Seq([Inh(p, DVar("X")); Inh(s, DVar("X"))]), int(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(p, m1), Inh(s, m2) when s <> p && m1 = m2 
                                        -> [(ConImp(Inh(p, IVar("X")), Inh(s, IVar("X"))), abd(tv1, tv2))
                                            (ConEqu(Inh(p, IVar("X")), Inh(s, IVar("X"))), com(tv1, tv2))
                                            (Par(set [Inh(p, DVar("X")); Inh(s, DVar("X"))]), int(tv1, tv2))
                                            (Equ(Inh(IVar("X"), s), Inh(IVar("X"), p)), com(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(m1, p), Inh(m2, s) when s <> p && m1 = m2 
                                        -> [(Imp(Inh(IVar("X"), s), Inh(IVar("X"), p)), ind(tv1, tv2))
                                            (And(set [Inh(DVar("X"), s); Inh(DVar("X"), p)]), int(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(m1, p), Inh(m2, s) when s <> p && m1 = m2 
                                        -> [(PreImp(Inh(IVar("X"), s), Inh(IVar("X"), p)), ind(tv1, tv2))
                                            (PreEqu(Inh(IVar("X"), s), Inh(IVar("X"), p)), com(tv1, tv2))
                                            (Seq([Inh(DVar("X"), s); Inh(DVar("X"), p)]), int(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(m1, p), Inh(m2, s) when s <> p && m1 = m2 
                                        -> [(ConImp(Inh(IVar("X"), s), Inh(IVar("X"), p)), ind(tv1, tv2))
                                            (ConEqu(Inh(IVar("X"), s), Inh(IVar("X"), p)), com(tv1, tv2))
                                            (Par(set [Inh(DVar("X"), s); Inh(DVar("X"), p)]), int(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(a, Inh(m1, p)), Inh(m2, s) when a <> Inh(m1, s) 
                                        -> [(Imp(And(set [a; Inh(IVar("Y"), s)]), Inh(IVar("Y"), p)), ind(tv1, tv2))
                                            (And(set [Imp(a, Inh(DVar("Y"), p)); Inh(DVar("Y"), s)]), int(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function AndPat(Inh(m1, p)::tl), Inh(m2, s) when m1 = m2 && s <> p 
                                        -> [(Imp(Inh(IVar("Y"), s), And(set (Inh(IVar("Y"), p)::tl))), ind(tv1, tv2))
                                            (And(set (Inh(DVar("Y"), s)::Inh(DVar("Y"), p)::tl)), int(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(a, Inh(p, m1)), Inh(s, m2) when s <> p && m1 = m2 && a <> Inh(s, m1) 
                                        -> [(Imp(And(set [a; Inh(p, IVar("Y"))]), Inh(s, IVar("Y"))), abd(tv1, tv2))
                                            (And(set [Imp(a, Inh(p, DVar("Y"))); Inh(s, DVar("Y"))]), int(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function AndPat(Inh(p, m1)::tl), Inh(s, m2) when s <> p && m1 = m2 
                                        -> [(Imp(Inh(s, IVar("Y")), And(set (Inh(p, IVar("Y"))::tl))), abd(tv1, tv2))
                                            (And(set (Inh(s, DVar("Y"))::Inh(p, DVar("Y"))::tl)), int(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function And(setA), Inh(m, s) when setA |> Set.contains (Inh(DVar("X"), s)) -> [(And(setA |> Set.remove (Inh(DVar("X"), s)) |> Set.add (Inh(m, s))), ana(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function And(setA), Inh(s, m) when setA |> Set.contains (Inh(s, DVar("X"))) -> [(And(setA |> Set.remove (Inh(s, DVar("X"))) |> Set.add (Inh(s, m))), ana(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(Inh(IVar(_), m1), c), Inh(s, m2) when m1 = m2 && c <> s && s <> m1 -> [(c, ded(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Imp(Inh(m1, IVar(_)), c), Inh(m2, s) when m1 = m2 && c <> s && m1 <> c -> [(c, ded(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function c, Imp(And(a_n), b) when a_n |> Set.contains c && b <> c -> [(Imp(And(a_n |> Set.remove c), b), ded(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function c1, Imp(Seq([c2; i]), b) when c1 = c2 && b <> c1 -> [(b, ded(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function b1, Imp(Seq(c::tl), b2) when b1 <> c -> [(c, abd(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(s, m), Imp(And(setA), b) when setA |> Set.contains (Inh(s, m)) -> [(Imp(And(setA |> Set.remove (Inh(s, m))), b), ded(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(s, m), Imp(And(setA), b) when setA |> Set.contains (Inh(s, m)) -> [(b, ded(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(s, m1), Imp(AndPat([c; i]), Inh(IVar(_), m2)) when m1 = m2 -> [(c, abd(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(m, s), Imp(And(setA), b) when setA |> Set.contains (Inh(m, IVar("1"))) -> [(b, ded(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function Inh(m1, s), Imp(AndPat([c; i]), Inh(m2, IVar(_))) when m1 = m2 -> [(c, ded(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function p, s when measureTime(s, p) && notImplication(p) && notImplication(s) 
                                        -> [(PreImp(Seq([s]), p), ind(tv1, tv2))
                                            (RetImp(Seq([s]), p), abd(tv1, tv2))
                                            (PreEqu(Seq([s]), p), com(tv1, tv2))
                                            (Seq([s; p]), int(tv1, tv2))] | _ -> [])
    (fun (tv1, tv2 : Truth) -> function p, s when concurrent(s, p) && notImplication(p) && notImplication(s) 
                                        -> [(ConImp(Seq([s]), p), ind(tv1, tv2))
                                            (ConImp(Seq([p]), s), ind(tv2, tv1))
                                            (ConEqu(Seq([s]), p), com(tv1, tv2))
                                            (Par(set [s; p]), int(tv1, tv2))] | _ -> [])
|]